package tr.edu.ege.kipler.satisfiability.blocking;

import java.util.Iterator;
import java.util.List;

import tr.edu.ege.kipler.satisfiability.container.ABox;
import tr.edu.ege.kipler.satisfiability.container.ConceptCategory;
import tr.edu.ege.kipler.satisfiability.container.Individual;
import tr.edu.ege.kipler.satisfiability.container.RBox;
import tr.edu.ege.kipler.satisfiability.container.operational.FilterType;
import tr.edu.ege.kipler.satisfiability.container.operational.RelatedIndividualWithTypeFilterFactory;
import tr.edu.ege.kipler.satisfiability.container.operational.SHIQAncestorCollector;
import tr.edu.ege.kipler.syntax.Role;
import tr.edu.ege.kipler.syntax.atomicformula.ObjectRoleAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.RoleAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.RoleAssertion.Type;
import tr.edu.ege.kipler.syntax.concept.Concept;
import tr.edu.ege.kipler.syntax.concept.QualifiedNoRestriction;
import tr.edu.ege.kipler.syntax.concept.RoleQuantification;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class OptimizedSHIQABoxBlocking extends SHIQABoxBlocking {

	protected boolean isBlockingConditionSatisfied(String indvName) {
		boolean result = false;
		Individual w = getABox().getIndividual(indvName);
		if (!getABox().isRoot(w)) {
			List<Individual> wAncestors = new SHIQAncestorCollector(getABox(),
					w).collect();
			if (wAncestors.size() >= 1) {
				Iterator<Individual> i = wAncestors.iterator();
				/*
				 * For the below part, I'll make the assumption that v is not a
				 * root node.
				 */
				// First element is guaranteed to be w's predecessor, i.e., v.
				Individual v = i.next();
				Individual wPrime = v;
				// wPrime can be found in the ancestors of w
				while (i.hasNext() && !result) {
					wPrime = i.next();
					result = bConditionsSatisfied(w, v, wPrime);
				}
				/*
				 * if wPrime is not in the (non-root) ancestors of w, then it
				 * can be the root node which is w's topmost ancestor's
				 * predecessor
				 */
				if (!result) {
					wPrime = getPredecessor(wPrime);
					result = bConditionsSatisfied(w, v, wPrime);
				}
			}
		}
		return result;
	}

	private boolean bConditionsSatisfied(Individual w, Individual v,
			Individual wPrime) {
		return b1(w, wPrime)
				&& b2(w, wPrime, v)
				&& ((b3(w, wPrime, v) && b4(w, wPrime, v)) || (b5(w, wPrime, v) && b6(
						w, v)));
	}

	public boolean isABlocked(ABox abox, String wStr, String vStr,
			String wPrimeStr) {
		setABox(abox);
		Individual w = getABox().getIndividual(wStr);
		Individual v = getABox().getIndividual(vStr);
		Individual wPrime = getABox().getIndividual(wPrimeStr);
		return b1(w, wPrime) && b2(w, wPrime, v) && b3(w, wPrime, v)
				&& b4(w, wPrime, v);
	}

	public boolean isCBlocked(ABox abox, String wStr, String vStr,
			String wPrimeStr) {
		setABox(abox);
		Individual w = getABox().getIndividual(wStr);
		Individual v = getABox().getIndividual(vStr);
		Individual wPrime = getABox().getIndividual(wPrimeStr);
		return b1(w, wPrime) && b2(w, wPrime, v) && b5(w, wPrime, v)
				&& b6(w, v);
	}

	private boolean b1(Individual w, Individual wPrime) {
		return wPrime.containsAllConceptsOf(w);
	}

	private boolean b2(Individual w, Individual wPrime, Individual v) {
		boolean result = true;
		Iterator<Concept> i = wPrime.conceptIterator(ConceptCategory.ALL);
		while (i.hasNext() && result) {
			RoleQuantification rq = (RoleQuantification) i.next();
			if (getABox().contains(
					new ObjectRoleAssertion(
							rq.getRole().copy().toggleInverse(), v.getName(), w
									.getName()))) {
				if (!v.contains(rq.getConcept())) {
					result = false;
					break;
				}
				RBox rbox = getABox().getWorld().getRBox();
				for (Role role : rbox.getSubRoles(rq.getRole())) {
					if (rbox.contains(new RoleAssertion(Type.TRANSITIVE, role))
							&& getABox().contains(
									new ObjectRoleAssertion(role.copy()
											.toggleInverse(), v.getName(), w
											.getName()))) {
						RoleQuantification newRq = new RoleQuantification(
								RoleQuantification.Constructor.ALL, role, rq
										.getConcept());
						if (!v.contains(newRq)) {
							result = false;
							break;
						}
					}
				}
			}
		}
		return result;
	}

	private boolean b3(Individual w, Individual wPrime, Individual v) {
		boolean result = true;
		Iterator<Concept> i = wPrime.conceptIterator(ConceptCategory.AT_MOST);
		while (i.hasNext() && result) {
			QualifiedNoRestriction qr = (QualifiedNoRestriction) i.next();
			ObjectRoleAssertion wInvSSuccessorOfv = new ObjectRoleAssertion(qr
					.getRole().copy().toggleInverse(), v.getName(), w.getName());
			if (getABox().contains(wInvSSuccessorOfv)
					&& v.contains(qr.getConcept())
					&& RelatedIndividualWithTypeFilterFactory.getFilter(
							FilterType.TYPED_SUCCESSOR, getABox(), wPrime,
							qr.getRole(), qr.getConcept()).filter().size() >= qr
							.getNo()) {
				result = false;
			}

		}
		return result;
	}

	private boolean b4(Individual w, Individual wPrime, Individual v) {
		boolean result = true;
		Iterator<Concept> i = wPrime.conceptIterator(ConceptCategory.AT_LEAST);
		while (i.hasNext() && result) {
			QualifiedNoRestriction qr = (QualifiedNoRestriction) i.next();
			ObjectRoleAssertion wInvTSuccessorOfv = new ObjectRoleAssertion(qr
					.getRole().copy().toggleInverse(), v.getName(), w.getName());
			result = isB4ConditionSatisfied(wPrime, qr.getRole(), qr
					.getConcept(), qr.getNo(), v, wInvTSuccessorOfv);
		}
		i = wPrime.conceptIterator(ConceptCategory.SOME);
		while (i.hasNext() && result) {
			RoleQuantification rq = (RoleQuantification) i.next();
			ObjectRoleAssertion wInvTSuccessorOfv = new ObjectRoleAssertion(rq
					.getRole().copy().toggleInverse(), v.getName(), w.getName());
			result = isB4ConditionSatisfied(wPrime, rq.getRole(), rq
					.getConcept(), 1, v, wInvTSuccessorOfv);
		}
		return result;
	}

	private boolean isB4ConditionSatisfied(Individual wPrime, Role role,
			Concept concept, int count, Individual v,
			ObjectRoleAssertion wInvTSuccessorOfv) {
		return RelatedIndividualWithTypeFilterFactory.getFilter(
				FilterType.TYPED_SUCCESSOR, getABox(), wPrime, role, concept)
				.filter().size() >= count
				|| (getABox().contains(wInvTSuccessorOfv) && v
						.contains(concept));
	}

	private boolean b5(Individual w, Individual wPrime, Individual v) {
		boolean result = true;
		Iterator<Concept> i = wPrime.conceptIterator(ConceptCategory.AT_MOST);
		while (i.hasNext() && result) {
			QualifiedNoRestriction qr = (QualifiedNoRestriction) i.next();
			ObjectRoleAssertion wInvTSuccessorOfv = new ObjectRoleAssertion(qr
					.getRole().copy().toggleInverse(), v.getName(), w.getName());
			if (getABox().contains(wInvTSuccessorOfv)
					&& v.contains(qr.getConcept())) {
				result = false;
			}
		}
		return result;
	}

	private boolean b6(Individual w, Individual v) {
		boolean result = true;
		Iterator<Concept> i = v.conceptIterator(ConceptCategory.AT_LEAST);
		while (i.hasNext() && result) {
			QualifiedNoRestriction qr = (QualifiedNoRestriction) i.next();
			ObjectRoleAssertion wUSuccessorOfv = new ObjectRoleAssertion(qr
					.getRole(), v.getName(), w.getName());
			if (getABox().contains(wUSuccessorOfv)
					&& w.contains(qr.getConcept())) {
				result = false;
			}
		}
		return result;
	}
}
